es:event_system{i:l}, e2,e1:es-E(es).
es-le(es; e1; e2)
 (n:. (0 < n)  (n < ||[e1, e2]||)  e(e1,e2].||[e1, es-pred(es; e)]|| = n  ) 

latex

Definitions

x:A. B(x), P  Q, es-le(es; e; e'), , es-locl(es; e; e'), t  T, prop{i:l}, x. t(x), P  Q, P  Q, e(e1,e2].P(e), x:A. B(x), A c B, P  Q, T, True, P  Q, top, subtype(S; T), wellfounded{i:l}(A; x,y.R(x;y)), x(s), guard(T), decidable(P), ||as||, Y, A, False

Lemmas

es-locl-wellfnd, es-locl wf, le wf, existse-between3 wf, Id wf, es-loc wf, not wf, assert wf, es-first wf, length wf1, es-interval wf, es-pred wf, es-le-loc, es-causl wf, es-loc-pred, es-locl-iff, event system wf, es-le-iff, nat wf, es-le wf, es-pred-locl, decidable lt, es-locl transitivity1, es-le weakening, squash wf, true wf, es-interval-less, es-le-pred, length-append, es-interval wf2, top wf, es-le-self, es-interval-eq